\begin{tabbing}
ma{-}rename(${\it rx}$;${\it ra}$;${\it rt}$;$M$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=mk{-}ma(fpf{-}rename(IdDeq;${\it rx}$;1of($M$));\+
\\[0ex]fpf{-}rename(KindDeq;$\lambda$$k$.kind{-}rename(${\it ra}$;${\it rt}$;$k$);1of(2of($M$)));
\\[0ex]fpf{-}rename(IdDeq;${\it rx}$;1of(2of(2of($M$))));
\\[0ex]fpf{-}rename(IdDeq;${\it ra}$;$\lambda$$f$,$s$,$v$. $f$(($s$$\,\circ\,$${\it rx}$),$v$) o 1of(2of(2of(2of($M$)))));
\\[0ex]f\=pf{-}rename(product{-}deq(Knd;Id;KindDeq;IdDeq);$\lambda$$p$.\=$\langle$kind{-}rename(${\it ra}$;${\it rt}$;1of($p$))\+\+
\\[0ex]$,\,$${\it rx}$(2of($p$))$\rangle$;$\lambda$$f$,$s$,$v$. $f$(($s$$\,\circ\,$${\it rx}$),$v$) o
\-\\[0ex]1of(2of(2of(2of(2of($M$))))));
\-\\[0ex]f\=pf{-}rename(product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);$\lambda$$p$.\=$\langle$kind{-}rename(${\it ra}$;${\it rt}$;1of($p$))\+\+
\\[0ex]$,\,$2of($p$)$\rangle$;$\lambda$$L$.map\=($\lambda$$p$.\=$\langle$${\it rt}$(1of($p$))\+\+
\\[0ex]$,\,$\=$\lambda$$s$,$v$.\+
\\[0ex]2of($p$)
\\[0ex](($s$$\,\circ\,$${\it rx}$)
\\[0ex],$v$)$\rangle$
\-\-\\[0ex];$L$) o
\-\-\\[0ex]1of(2of(2of(2of(2of(2of($M$)))))));
\-\\[0ex]f\=pf{-}rename(IdDeq;${\it rx}$;$\lambda$$L$.map($\lambda$$k$.kind{-}rename(${\it ra}$;${\it rt}$;$k$);$L$) o\+
\\[0ex]1of(2of(2of(2of(2of(2of(2of($M$))))))));
\-\\[0ex]fpf{-}rename(product{-}deq(IdLnk;Id;IdLnkDeq;IdDeq);$\lambda$$p$.$\langle$1of($p$)$,\,$${\it rt}$(2of($p$))$\rangle$;$\lambda$$L$.
\\[0ex]map($\lambda$$k$.kind{-}rename(${\it ra}$;${\it rt}$;$k$);$L$) o 1of(2of(2of(2of(2of(2of(2of(2of($M$)))))))));
\\[0ex]f\=pf{-}rename(KindDeq;$\lambda$$k$.kind{-}rename(${\it ra}$;${\it rt}$;$k$);$\lambda$$L$.map(${\it rx}$;$L$) o\+
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of($M$))))))))));
\-\\[0ex]fpf{-}rename(KindDeq;$\lambda$$k$.kind{-}rename(${\it ra}$;${\it rt}$;$k$);1of(\=2of(2of(2of(2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M$)))))))))));
\-\\[0ex]f\=pf{-}rename(IdDeq;${\it rx}$;$\lambda$$L$.map($\lambda$$k$.kind{-}rename(${\it ra}$;${\it rt}$;$k$);$L$) o\+
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of($M$)))))))))))))
\-\-
\end{tabbing}